$\forall$$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $T$:Type, ${\it es}$:ES.
\\[0ex]es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)
\\[0ex]$\Rightarrow$ vartype($i$;"ecl") $\subseteq\rho$ $T$
\\[0ex]$\Rightarrow$ $\neg$"ecl" $\in$ dom(${\it ds}$)
\\[0ex]$\Rightarrow$ es{-}decls(${\it es}$;$i$;${\it ds}$ $\oplus$ "ecl" : $T$;${\it da}$)